T:Type, R:(TT).
(a, b:T. Dec(R(a,b)))  (connex(T;R)  {a, b:T. ((R\)(a,b))  ((R)(a,b))  ((R\)(b,a))}) 

latex

Up	gen algebra 1
Definitions of Statement	connex(T;R), E, E\
Definitions	E, E\, connex(T;R), Symmetrize(x,y.R(x;y);a;b), strict_part(x,y.R(x;y);a;b), x(s1,s2)
Lemmas	connex iff trichot